/*
 * Copyright 2014, General Dynamics C4 Systems
 *
 * SPDX-License-Identifier: GPL-2.0-only
 */

#pragma once

#include <config.h>
#include <api/types.h>
#include <stdint.h>
#include <arch/object/structures_gen.h>
#include <mode/types.h>
#include <sel4/macros.h>
#include <sel4/arch/constants.h>
#include <sel4/sel4_arch/constants.h>
#include <benchmark/benchmark_utilisation_.h>

enum irq_state {
    IRQInactive  = 0,   /*Z 禁用 */
    IRQSignal    = 1,   /*Z 未禁用其它IRQ */
    IRQTimer     = 2,   /*Z 定时器IRQ */
#ifdef ENABLE_SMP_SUPPORT
    IRQIPI       = 3,   /*Z IPI IRQ */
#endif
    IRQReserved         /*Z 保留(包括IOMMU中断) */
};
typedef word_t irq_state_t;/*Z 硬件中断基本属性 */
/*Z 调度域数据结构 */
typedef struct dschedule {
    dom_t domain;   /*Z 调度域 */
    word_t length;  /*Z 域时间片(毫秒) */
} dschedule_t;

enum asidSizeConstants {
    asidHighBits = seL4_NumASIDPoolsBits,   /*Z 高3位为池选择位 */
    asidLowBits = seL4_ASIDPoolIndexBits    /*Z 低9位为池内索引位 */
};

/* Arch-independent object types */
enum endpoint_state {
    EPState_Idle = 0,   /*Z 无线程 */
    EPState_Send = 1,   /*Z 队列线程都要发 */
    EPState_Recv = 2    /*Z 队列线程都要收 */
};
typedef word_t endpoint_state_t;    /*Z EP队列状态(各状态是互斥的) */

enum notification_state {
    NtfnState_Idle    = 0,  /*Z 空闲 */
    NtfnState_Waiting = 1,  /*Z 队列线程在等待通知 */
    NtfnState_Active  = 2   /*Z 活跃-通知已到但还无人接收 */
};
typedef word_t notification_state_t;/*Z NF队列状态(各状态是互斥的) */

#define EP_PTR(r) ((endpoint_t *)(r))       /*Z 将参数强制转换成端点指针 */
#define EP_REF(p) ((word_t)(p))             /*Z 将参数强制转换成word_t */

#define NTFN_PTR(r) ((notification_t *)(r)) /*Z 将参数强制转换成通知指针 */
#define NTFN_REF(p) ((word_t)(p))           /*Z 将参数强制转换成word_t */

#define CTE_PTR(r) ((cte_t *)(r))           /*Z 将参数强制转换成CSlot指针 */
#define CTE_REF(p) ((word_t)(p))            /*Z 将参数强制转换成word_t */

#define CNODE_MIN_BITS 1
#define CNODE_PTR(r) (CTE_PTR(r))           /*Z CNode指针即CSlot指针 */
#define CNODE_REF(p) (CTE_REF(p)>>CNODE_MIN_BITS)

// We would like the actual 'tcb' region (the portion that contains the tcb_t) of the tcb
// to be as large as possible, but it still needs to be aligned. As the TCB object contains
// two sub objects the largest we can make either sub object whilst preserving size alignment
// is half the total size. To halve an object size defined in bits we just subtract 1
#define TCB_SIZE_BITS (seL4_TCBBits - 1)/*Z 10。TCB由CNode和tcb_t两部分构成，2K对齐。这里的值是说一家一半 */

#define TCB_CNODE_SIZE_BITS (TCB_CNODE_RADIX + seL4_SlotBits)
#define TCB_CNODE_RADIX     4   /*Z TCB CNode索引位位数。剩下的512字节干什么用??? */
#define TCB_OFFSET          BIT(TCB_SIZE_BITS)  /*Z 1K */

/* Generate a tcb_t or cte_t pointer from a tcb block reference */
#define TCB_PTR(r)       ((tcb_t *)(r))         /*Z 将参数强制转换成TCB指针 */
#define TCB_CTE_PTR(r,i) (((cte_t *)(r))+(i))
#define TCB_REF(p)       ((word_t)(p))          /*Z 将参数强制转换成word_t */
/*Z tcb_t指针2K对齐从页指向TCB CNode，将第i个word_t项强制转换成CSlot指针。注意i不能超过64（总大小1K） */
/* Generate a cte_t pointer from a tcb_t pointer */
#define TCB_PTR_CTE_PTR(p,i) \
    (((cte_t *)((word_t)(p)&~MASK(seL4_TCBBits)))+(i))

#define SC_REF(p) ((word_t) (p))                /*Z 将参数强制转换成word_t */
#define SC_PTR(r) ((sched_context_t *) (r))     /*Z 将参数强制转换成SC(调度上下文)指针 */

#define REPLY_REF(p) ((word_t) (p))         /*Z 将参数强制转换成word_t指针 */
#define REPLY_PTR(r) ((reply_t *) (r))      /*Z 将参数强制转换成reply_t指针 */

#define WORD_PTR(r) ((word_t *)(r))
#define WORD_REF(p) ((word_t)(p))           /*Z 将参数强制转换成word_t */

#define ZombieType_ZombieTCB        BIT(wordRadix)          /*Z 64。指代Zombie能力类型是TCB */
#define ZombieType_ZombieCNode(n)   ((n) & MASK(wordRadix)) /*Z <64。指代其它Zombie能力类型 */
/*Z 拼接Zombie能力：原始地址ptr与容量number掩码成ID，type指明掩码位数(实际还多1位) */
static inline cap_t CONST Zombie_new(word_t number, word_t type, word_t ptr)
{
    word_t mask;

    if (type == ZombieType_ZombieTCB) {/*Z TCB */
        mask = MASK(TCB_CNODE_RADIX + 1);
    } else {
        mask = MASK(type + 1);
    }
    /*Z 用type+1可从ID中恢复出原始地址 */
    return cap_zombie_cap_new((ptr & ~mask) | (number & mask), type);
}
/*Z 获取Zombie能力ID的拼接掩码位数(实际还要加1) */
static inline word_t CONST cap_zombie_cap_get_capZombieBits(cap_t cap)
{
    word_t type = cap_zombie_cap_get_capZombieType(cap);
    if (type == ZombieType_ZombieTCB) {
        return TCB_CNODE_RADIX;
    }
    return ZombieType_ZombieCNode(type); /* cnode radix */
}
/*Z 获取Zombie能力的容量 */
static inline word_t CONST cap_zombie_cap_get_capZombieNumber(cap_t cap)
{
    word_t radix = cap_zombie_cap_get_capZombieBits(cap);
    return cap_zombie_cap_get_capZombieID(cap) & MASK(radix + 1);
}
/*Z 获取Zombie能力的原始地址 */
static inline word_t CONST cap_zombie_cap_get_capZombiePtr(cap_t cap)
{
    word_t radix = cap_zombie_cap_get_capZombieBits(cap);
    return cap_zombie_cap_get_capZombieID(cap) & ~MASK(radix + 1);
}

static inline cap_t CONST cap_zombie_cap_set_capZombieNumber(cap_t cap, word_t n)
{
    word_t radix = cap_zombie_cap_get_capZombieBits(cap);
    word_t ptr = cap_zombie_cap_get_capZombieID(cap) & ~MASK(radix + 1);
    return cap_zombie_cap_set_capZombieID(cap, ptr | (n & MASK(radix + 1)));
}

/* Capability table entry (CTE) */
struct cte {
    cap_t cap;              /*Z u64[2] */
    mdb_node_t cteMDBNode;  /*Z u64[2] */
};
typedef struct cte cte_t;   /*Z CSlot */
/*Z 空MDB节点 */
#define nullMDBNode mdb_node_new(0, false, false, 0)

/* Thread state *//*Z 共9种 */
enum _thread_state {
    ThreadState_Inactive = 0,
    ThreadState_Running,                /*Z 可运行。运行中 */
    ThreadState_Restart,                /*Z 可运行。估计是充值后的状态 */
    ThreadState_BlockedOnReceive,       /*Z 阻塞于IPC接收中 */
    ThreadState_BlockedOnSend,          /*Z 阻塞于IPC发送中 */
    ThreadState_BlockedOnReply,         /*Z 阻塞于接收回复中 */
    ThreadState_BlockedOnNotification,  /*Z 阻塞于接收通知中 */
#ifdef CONFIG_VTX
    ThreadState_RunningVM,              /*Z 可运行。运行或准备运行在VM状态 */
#endif
    ThreadState_IdleThreadState         /*Z idle线程 */
};
typedef word_t _thread_state_t; /*Z 线程状态 */
/*Z TCB CNode中有固定位置的能力索引 */
/* A TCB CNode and a TCB are always allocated together, and adjacently.
 * The CNode comes first. */
enum tcb_cnode_index {
    /* CSpace root */
    tcbCTable = 0,  /*Z 根CNode访问能力 */
    /*Z 即一级页表访问能力 */
    /* VSpace root */
    tcbVTable = 1,

#ifdef CONFIG_KERNEL_MCS
    /* IPC buffer cap slot *//*Z 即IPC buffer访问能力 */
    tcbBuffer = 2,
/*Z 当设置了这个能力后，在线程出现例外时将触发这个能力指向的线程；如果未设置则本线程将成为再也无法执行的僵尸 */
    /* Fault endpoint slot */
    tcbFaultHandler = 3,/* V 当异常时发出异常信号给另一个函数，本身不作为异常处理线程 */
/*Z 当设置了这个能力后，在线程用完预算后将触发这个能力指向的线程 */
    /* Timeout endpoint slot */
    tcbTimeoutHandler = 4,
#else
    /*Z 回复能力，要求方设置 */
    /* Reply cap slot */
    tcbReply = 2,
    /*Z 回复能力，被要求方接收 */
    /* TCB of most recent IPC sender */
    tcbCaller = 3,
    /*Z IPC buffer访问能力(页能力)。注意：是对IPC行为的限制，而不是限制内存访问 */
    /* IPC buffer cap slot */
    tcbBuffer = 4,
#endif
    tcbCNodeEntries
};
typedef word_t tcb_cnode_index_t;

#include <arch/object/structures.h>

struct user_data {
    word_t words[BIT(seL4_PageBits) / sizeof(word_t)];
};
typedef struct user_data user_data_t;

struct user_data_device {
    word_t words[BIT(seL4_PageBits) / sizeof(word_t)];
};
typedef struct user_data_device user_data_device_t;
/*Z 类型转换为word_t */
static inline word_t CONST wordFromVMRights(vm_rights_t vm_rights)
{
    return (word_t)vm_rights;
}
/*Z 强制类型转换 */
static inline vm_rights_t CONST vmRightsFromWord(word_t w)
{
    return (vm_rights_t)w;
}
/*Z 将字转换成vm_attributes_t类型，struct {u64[1]} */
static inline vm_attributes_t CONST vmAttributesFromWord(word_t w)
{
    vm_attributes_t attr;/*Z struct {u64[1]} */

    attr.words[0] = w;
    return attr;
}

#ifdef CONFIG_KERNEL_MCS
typedef struct sched_context sched_context_t;
typedef struct reply reply_t;/*Z 回复类型 */
#endif
/*Z tcb_t大小不超过1K */
/* TCB: size >= 18 words + sizeof(arch_tcb_t) + 1 word on MCS (aligned to nearest power of 2) */
struct tcb {
    /* arch specific tcb state (including context)*//*Z 架构有关的状态 */
    arch_tcb_t tcbArch;
    /*Z 线程状态，数据结构是struct{u64[3]}     阻塞的IPC对象可能有EP、NF、reply指针
    u64[0]  47              4         3  0
            阻塞的IPC对象指针         状态
    u64[1]        3                 2                1            0
            能否授权别人   能否授权别人回复    是否需回复    是否在ready/release队列
    u64[2]  标记
    */
    /* Thread state, 3 words */
    thread_state_t tcbState;

    /* Notification that this TCB is bound to. If this is set, when this TCB waits on
     * any sync endpoint, it may receive a signal from a Notification object.
     * 1 word*//*Z 绑定Notification对象后，该线程在等待IPC通信时也会收到通知信号 */
    notification_t *tcbBoundNotification;
    /*Z 当前要通过IPC发送的错误 */
    /* Current fault, 2 words */
    seL4_Fault_t tcbFault;
    /*Z 当前要通过IPC发送的查询类错误 */
    /* Current lookup failure, 2 words */
    lookup_fault_t tcbLookupFailure;
    /*Z 线程所属的调度域。猜测不同的域之间无法或很难通信 */
    /* Domain, 1 byte (padded to 1 word) */
    dom_t tcbDomain;
    /*Z 最大可控优先级。该线程生成其它线程时，设置的优先级也不能超过此项 */
    /*  maximum controlled priority, 1 byte (padded to 1 word) */
    prio_t tcbMCP;
    /*Z seL4采用抢占的、有优先级的(同级轮转)、tickless调度算法 */
    /* Priority, 1 byte (padded to 1 word) */
    prio_t tcbPriority;

#ifdef CONFIG_KERNEL_MCS
    /* scheduling context that this tcb is running on, if it is NULL the tcb cannot
     * be in the scheduler queues, 1 word *//*Z 指向其调度上下文。一一对应 */
    sched_context_t *tcbSchedContext;
    /*Z 受让者SC */
    /* scheduling context that this tcb yielded to */
    sched_context_t *tcbYieldTo;
#else
    /*Z 定时器递减的可运行时间片 */
    /* Timeslice remaining, 1 word */
    word_t tcbTimeSlice;
    /*Z 错误处理CSlot句柄。指示的是个EP能力 */
    /* Capability pointer to thread fault handler, 1 word */
    cptr_t tcbFaultHandler;
#endif
    /*Z IPC buffer虚拟地址 */
    /* userland virtual address of thread IPC buffer, 1 word */
    word_t tcbIPCBuffer;

#ifdef ENABLE_SMP_SUPPORT
    /* cpu ID this thread is running on, 1 word */
    word_t tcbAffinity;/*Z 线程亲和cpu。不是亲和cpu不会直接调度。MCS不用此字段。没有显式系统调用，内核不会在core间迁移TCB，也就是内核不提供负载均衡功能 */
#endif /* ENABLE_SMP_SUPPORT */
    /*Z 双向ready调度队列指针，也用于MCS的待充值队列 */
    /* Previous and next pointers for scheduler queues , 2 words */
    struct tcb *tcbSchedNext;
    struct tcb *tcbSchedPrev;
    /* Preivous and next pointers for endpoint and notification queues, 2 words */
    struct tcb *tcbEPNext;  /*Z EP、NF队列指针 */
    struct tcb *tcbEPPrev;

#ifdef CONFIG_KERNEL_MCS
    /* if tcb is in a call, pointer to the reply object, 1 word */
    reply_t *tcbReply;  /*Z reply能力。实际是一次性对象，这时已与通信的EP无关，该对象也于CSpace无关 */
#endif
#ifdef CONFIG_BENCHMARK_TRACK_UTILISATION
    /* 16 bytes (12 bytes aarch32) */
    benchmark_util_t benchmark;
#endif

#ifdef CONFIG_DEBUG_BUILD
    /* Pointers for list of all tcbs that is maintained
     * when CONFIG_DEBUG_BUILD is enabled, 2 words */
    struct tcb *tcbDebugNext;/*Z 亲和cpu的DEBUG线程双向链表后向指针 */
    struct tcb *tcbDebugPrev;/*Z 亲和cpu的DEBUG线程双向链表前向指针 */
    /* Use any remaining space for a thread name */
    char tcbName[];/*Z 至1K大小处均用作线程名 */
#endif /* CONFIG_DEBUG_BUILD */
};
typedef struct tcb tcb_t;
/*Z 充值单元，头单元为当前预算。轮转线程(scPeriod=0)只根据rAmount轮流转；对其它(零散)线程，至少要经过scPeriod */
#ifdef CONFIG_KERNEL_MCS
typedef struct refill {
    /* Absolute timestamp from when this refill can be used */
    ticks_t rTime;      /*Z 预算启用时间 */
    /* Amount of ticks that can be used from this refill */
    ticks_t rAmount;    /*Z 可用的预算值(时间片TICKs) */
} refill_t;
/*Z 最少充值队列元素个数 */
#define MIN_REFILLS 2u
/*Z 在配置MCS扩展的情况下，每个线程必须绑定一个SCO（调度上下文）对象。据此，线程时间片有严格的上限，适用于实时系统 */
struct sched_context {
    /*Z 充值周期。每周期运行一个预算。scPeriod不小于budget，但用0表示RoundRobin调度 */
    /* period for this sc -- controls rate at which budget is replenished  V 控制预算的补充率*/
    ticks_t scPeriod;
    /*Z 累加的已消费的时间。Consumed系统调用和超时错误后复位 */
    /* amount of ticks this sc has been scheduled for since seL4_SchedContext_Consumed
     * was last called or a timeout exception fired */
    ticks_t scConsumed;
    /*Z SC对应的cpu。没有显式系统调用，内核不会在core间迁移SC，也就是内核不提供负载均衡功能 */
    /* core this scheduling context provides time for - 0 if uniprocessor */
    word_t scCore;
    /*Z 本调度上下文(SC)对应的TCB。一一对应 */
    /* thread that this scheduling context is bound to */
    tcb_t *scTcb;

    /* if this is not NULL, it points to the last reply object that was generated
     * when the scheduling context was passed over a Call */
    reply_t *scReply;

    /* notification this scheduling context is bound to
     * (scTcb and scNotification cannot be set at the same time) */
    notification_t *scNotification;
    /*Z 调度上下文标记 */
    /* data word that is sent with timeout faults that occur on this scheduling context */
    word_t scBadge;
    /*Z 出让者 */
    /* thread that yielded to this scheduling context */
    tcb_t *scYieldFrom;

    /* Amount of refills this sc tracks */
    word_t scRefillMax;     /*Z 充值循环队列元素数量上限 */
    /* Index of the head of the refill circular buffer */
    word_t scRefillHead;    /*Z 充值循环队列头索引 */
    /* Index of the tail of the refill circular buffer */
    word_t scRefillTail;    /*Z 充值循环队列尾索引 */
};/*Z 大小是11个字。从这往后到SC尾是refill队列 */

struct reply {  /*Z 调用线程必须保持等待回复状态，否则该对象将自动销毁 */
    /* TCB pointed to by this reply object. This pointer reflects two possible relations, depending
     * on the thread state.
     *
     * ThreadState_BlockedOnReply: this tcb is the caller that is blocked on this reply object,
     * ThreadState_BlockedOnRecv: this tcb is the callee blocked on an endpoint with this reply object.
     *
     * The back pointer for this TCB is stored in the thread state.*/
    tcb_t *replyTCB;    /*Z reply能力实际上指向对方TCB的指针，对方的线程状态为阻塞于该reply对象 */

    /* 0 if this is the start of the call chain, or points to the
     * previous reply object in a call chain */
    call_stack_t replyPrev;

    /* Either a scheduling context if this reply object is the head of the call chain
     * (the last caller before the server) or another reply object. 0 if no scheduling
     * context was passed along the call chain */
    call_stack_t replyNext;
};
#endif

/* Ensure object sizes are sane */
compile_assert(cte_size_sane, sizeof(cte_t) <= BIT(seL4_SlotBits))
compile_assert(tcb_cte_size_sane, TCB_CNODE_SIZE_BITS <= TCB_SIZE_BITS)
compile_assert(tcb_size_sane,
               BIT(TCB_SIZE_BITS) >= sizeof(tcb_t))
compile_assert(tcb_size_not_excessive,
               BIT(TCB_SIZE_BITS - 1) < sizeof(tcb_t))
compile_assert(ep_size_sane, sizeof(endpoint_t) <= BIT(seL4_EndpointBits))
compile_assert(notification_size_sane, sizeof(notification_t) <= BIT(seL4_NotificationBits))

/* Check the IPC buffer is the right size */
compile_assert(ipc_buf_size_sane, sizeof(seL4_IPCBuffer) == BIT(seL4_IPCBufferSizeBits))
#ifdef CONFIG_KERNEL_MCS
compile_assert(sc_core_size_sane, (sizeof(sched_context_t) + MIN_REFILLS *sizeof(refill_t) <=
                                   seL4_CoreSchedContextBytes))
compile_assert(reply_size_sane, sizeof(reply_t) <= BIT(seL4_ReplyBits))
compile_assert(refill_size_sane, (sizeof(refill_t) == seL4_RefillSizeBytes))
#endif

/* helper functions */
/*Z 能力类型是否和架构相关 */
static inline word_t CONST isArchCap(cap_t cap)
{
    return (cap_get_capType(cap) % 2);
}
/*Z 返回能力所指代的对象大小(位数表示) */
static inline word_t CONST cap_get_capSizeBits(cap_t cap)
{

    cap_tag_t ctag;

    ctag = cap_get_capType(cap);

    switch (ctag) {
    case cap_untyped_cap:
        return cap_untyped_cap_get_capBlockSize(cap);

    case cap_endpoint_cap:
        return seL4_EndpointBits;

    case cap_notification_cap:
        return seL4_NotificationBits;

    case cap_cnode_cap:
        return cap_cnode_cap_get_capCNodeRadix(cap) + seL4_SlotBits;

    case cap_thread_cap:
        return seL4_TCBBits;

    case cap_zombie_cap: {
        word_t type = cap_zombie_cap_get_capZombieType(cap);
        if (type == ZombieType_ZombieTCB) {
            return seL4_TCBBits;
        }
        return ZombieType_ZombieCNode(type) + seL4_SlotBits;
    }

    case cap_null_cap:
        return 0;

    case cap_domain_cap:
        return 0;

    case cap_reply_cap:
#ifdef CONFIG_KERNEL_MCS
        return seL4_ReplyBits;
#else
        return 0;
#endif

    case cap_irq_control_cap:
#ifdef CONFIG_KERNEL_MCS
    case cap_sched_control_cap:
#endif
        return 0;

    case cap_irq_handler_cap:
        return 0;

#ifdef CONFIG_KERNEL_MCS
    case cap_sched_context_cap:
        return cap_sched_context_cap_get_capSCSizeBits(cap);
#endif

    default:
        return cap_get_archCapSizeBits(cap);
    }

}
/*Z 能力是否与内存有关 */
/* Returns whether or not this capability has memory associated
 * with it or not. Referring to this as 'being physical' is to
 * match up with the Haskell and abstract specifications */
static inline bool_t CONST cap_get_capIsPhysical(cap_t cap)
{
    cap_tag_t ctag;

    ctag = cap_get_capType(cap);

    switch (ctag) {
    case cap_untyped_cap:
        return true;

    case cap_endpoint_cap:
        return true;

    case cap_notification_cap:
        return true;

    case cap_cnode_cap:
        return true;

    case cap_thread_cap:
#ifdef CONFIG_KERNEL_MCS
    case cap_sched_context_cap:
#endif
        return true;

    case cap_zombie_cap:
        return true;

    case cap_domain_cap:
        return false;

    case cap_reply_cap:
#ifdef CONFIG_KERNEL_MCS
        return true;
#else
        return false;
#endif

    case cap_irq_control_cap:
#ifdef CONFIG_KERNEL_MCS
    case cap_sched_control_cap:
#endif
        return false;

    case cap_irq_handler_cap:
        return false;

    default:
        return cap_get_archCapIsPhysical(cap);
    }
}
/*Z 根据能力类型获取其所指对象的地址 */
static inline void *CONST cap_get_capPtr(cap_t cap)
{   /*Z 能力类型枚举 */
    cap_tag_t ctag;
    /*Z 获取能力的类型 */
    ctag = cap_get_capType(cap);

    switch (ctag) {
    case cap_untyped_cap:
        return WORD_PTR(cap_untyped_cap_get_capPtr(cap));

    case cap_endpoint_cap:
        return EP_PTR(cap_endpoint_cap_get_capEPPtr(cap));

    case cap_notification_cap:
        return NTFN_PTR(cap_notification_cap_get_capNtfnPtr(cap));

    case cap_cnode_cap:
        return CTE_PTR(cap_cnode_cap_get_capCNodePtr(cap));

    case cap_thread_cap:
        return TCB_PTR_CTE_PTR(cap_thread_cap_get_capTCBPtr(cap), 0);

    case cap_zombie_cap:    /*Z ??????? 未看 */
        return CTE_PTR(cap_zombie_cap_get_capZombiePtr(cap));

    case cap_domain_cap:
        return NULL;

    case cap_reply_cap:
#ifdef CONFIG_KERNEL_MCS
        return REPLY_PTR(cap_reply_cap_get_capReplyPtr(cap));
#else
        return NULL;
#endif

    case cap_irq_control_cap:
#ifdef CONFIG_KERNEL_MCS
    case cap_sched_control_cap:
#endif
        return NULL;

    case cap_irq_handler_cap:
        return NULL;

#ifdef CONFIG_KERNEL_MCS
    case cap_sched_context_cap:
        return SC_PTR(cap_sched_context_cap_get_capSCPtr(cap));
#endif

    default:
        return cap_get_archCapPtr(cap);

    }
}
/*Z 导出能力相对于源能力是否可撤销 */
static inline bool_t CONST isCapRevocable(cap_t derivedCap, cap_t srcCap)
{
    if (isArchCap(derivedCap)) {
        return Arch_isCapRevocable(derivedCap, srcCap);
    }
    switch (cap_get_capType(derivedCap)) {
    case cap_endpoint_cap:/*Z 对于端点能力，导出的不同标记的能力是可撤销的 */
        return (cap_endpoint_cap_get_capEPBadge(derivedCap) !=
                cap_endpoint_cap_get_capEPBadge(srcCap));

    case cap_notification_cap:/*Z 对于通知能力，导出的不同标记的能力是可撤销的 */
        return (cap_notification_cap_get_capNtfnBadge(derivedCap) !=
                cap_notification_cap_get_capNtfnBadge(srcCap));

    case cap_irq_handler_cap:/*Z 对于中断控制能力，导出的中断处理能力是可撤销的 */
        return (cap_get_capType(srcCap) ==
                cap_irq_control_cap);

    case cap_untyped_cap:/*Z 对于未映射页能力，都是可撤销的 */
        return true;

    default:/*Z 其它都是不可撤销的 */
        return false;
    }
}

